интуиционистская логика

интуиционистская логика
        ИНТУИЦИОНИСТСКАЯ ЛОГИКА — первоначально появилась как логика интуиционистской математики, но затем область ее применения чрезвычайно расширилась. Неформально И.л. начал развивать Л. Брауэр в 1907; первую интерпретацию, независимую от интуиционистской математики, дал А.Н. Колмогоров; первую формализацию построил А. Гейтинг.
        Язык И. л. совпадает с языком классической логики. Правила естественного вывода для всех связок, кроме отрицания, также можно оставить неизменными. Для отрицания правило снятия двойного отрицания ослабляется до правила «Из лжи следует все что угодно».
        В И. л. все связки независимы. В ней нет стандартных форм, аналогичных классическим. Как правило, преобразования, связанные с законами формулировки отрицаний и приведения к предваренной форме, действуют лишь в одну сторону. Так, напр., верно -AW-B-,A8LB), а -А & В)=> -A v -£ выполнено не всегда.
        Слабый закон исключенного третьего «А и его отрицание не могут быть одновременно ложны» сохраняется и в И.л. в форме —1 —I (А V —А), отвергается как логический закон лишь (A v -А). Поэтому неправильно трактовать И. л. как вводящую дополнительные истинностные значения; она, скорее, отвергает саму концепцию логических значений. И. л. не может быть описана конечной системой логических значений.
        Для И. л. выполнено свойство корректности относительно V и 3: если доказано А V В, то доказано либо А, либо В; если доказано ЗхА(х), то для некоторого t доказано A(t). Данным свойством классическая логика не обладает. Классическая логика вкладывается в интуиционистскую. Первым такое погружение построил Гливенко.
        И. л. имеет несколько математических интерпретаций. Исторически первой была интерпретация А. Тарского. В ней значениями истинности для предикатов являются открытые подмножества топологического пространства. Значения & v3 определяются булевым образом. Значение —А есть внутренность дополнения значения А. Напр., несправедливость А V —А можно продемонстрировать следующим образом: объединение открытого единичного круга и внутренности его дополнения дает плоскость без единичной окружности. Следующей интерпретацией стала алгебраическая. Еще одна семантика И.л. берет начало от Бета и развита Крипке. Это — один из видов моделей Крипке (см. Семантика возможных миров).
        Параллельно с этим развивалась линия, ведущая начало от содержательного смысла И. л. согласно Брауэру. Формулы истолковывались как задачи, логические связки — как преобразования задач, аксиомы — как задачи, для которых решения считаются известными; правила вывода — как преобразования решений задач. Данные идеи систематизировал А.Н. Колмогоров. Каждой формуле А сопоставляется множество ее реализаций '. Каждая реализация считается решением задачи, соответствующей А.
        Реализации элементарных формул задаются по определению. ® & В) - ®Ах©В. ® V В) = ®АФ®В. ®-пА=<=>®А=0. ®ЗхА(х)=Фаеи®А(а). Реализациями А => В являются эффективные функционалы из ©А в ®В. Реализациями являются эффективные функционалы, перерабатывающие каждое aeU в реализацию А(а). Уникальным свойством И. л. является наличие двух разнородных и несводимых друг к другу классов семантик: реализуемостей и моделей Крипке.
        В данном определении остается не уточненным понятие эффективного функционала. В частности, если взять в качестве эффективных функционалов все классические функции, то логика превращается в классическую. С.К. Клини построил первый точный вариант реализуемости, взяв в качестве эффективных операторов алгоритмы и кодируя программы алгоритмов натуральными числами, обходя, таким образом, сложности с операторами высших типов (клиниевская реализуемость). Он показал, что из доказательства в интуиционистской арифметике извлекается клиниевская реализация доказанной теоремы и поэтому если мы доказали ЗхА(х), то имеется такое п, что доказано А(п). Это точно обосновало тезис Брауэра, что интуиционистские доказательства дают построения.
        Обобщения идеи Колмогорова на другие классы построений с ограниченными ресурсами показали, что идея конструктивности не является исключительной принадлежностью И. л. Другим классам построений соответствуют другие конструктивные логики, чаще всего противоречащие как классической логике, так и И. л. Напр., в линейных логиках не принимается закон А = > А & А, в нильпотентных А = > А влечет -А, и т. д. Поскольку разные классы построений противоречат друг другу уже на логическом уровне, то совместное их использование приводит к грубым концептуальным противоречиям и, соответственно, к нежелательным практическим эффектам. Поэтому система конструктивных логик стала основой для системы стилей программирования, а И. л. занимает в ней место логики структурного программирования.
        Аналогия между доказательствами в И. л. и построениями усилена в [1]. Замкнутые типизированные выражения в комбинаторной логике изоморфны выводам в гильбертовской формулировке импликативного фрагмента И. л. Замкнутые типизированные А. -термы изоморфны выводам в импликативном фрагменте естественного вывода. Изоморфизм между выводами и Х -термами пытались расширить на всю И. л. Но на его пути стоит препятствие, указанное еще Брауэром и явно выделенное НА. Шаниным. Выводы в И. л. соединяют построения и их обоснования. В частности, построения, проделанные при выводе -iA, нельзя вычислять, поскольку они приведут к ошибке. Такие объекты, которые нельзя или не нужно вычислять в программе, но нужно рассматривать для ее обоснования, Г. С. Цейтин назвал призраками. НА. Шанин рассмотрел алгоритм конструктивной расшифровки, разбивающий формулу на задачу и обоснование решения, причем вторая часть может в рамках конструктивного направления в математике доказываться классически. Дан алгоритм классификации объектов вывода в И. л., отделяющий построения и призраки.
        И. л. варьировали многими способами. В минимальной логике Иогансона отбрасывается ex falso quodlibet. Как оказалось, в прикладных теориях интуиционистское отрицание моделируется (напр., в теории натуральных чисел как А = > 0=1). Г р и с предложил симметрическую И. л., в которой истина и ложь равноправны. В симметрической И. л. сохраняются обычные правила формулировки отрицаний классической логики. Отрицание в ней обычно обозначается =>А, интерпретируется как задача построения контрпримера к А и называется сильным отрицанием или конструктивным опровержением. Симметрическая И. л. детально исследована в монографии И.Д. Заславского.
        Н.Н. Непейвода
        Лит.: Шанин Н.А. О конструктивном понимании математических суждений // Тр. матем. ин-та им. В. А. Стеклова. Т. 52; Непейвода Н.Н. О построении правильных программ // Вопросы кибернетики. Т. 46. 1978; Непейвода Н.Н., Скопин Н.Н. Основания программирования. Ижевск—Москва, 2003; Brouwer L.E.J. Over de grondslagen der wiskunde [Об основаниях знания]. Amsterdam — Leipzig, 1907; Brouwer L.E.J. De onbetrouwbaarheid der logische principes [О недостоверности логических принципов] // Tijdskrift. Wijsbegeerte. Vol. 2. 1908; HeytingA. Die formalen Regeln der intuitionistischen Logik // Sitz. Berlin, 1930; Колмогоров А.Н. Zur Deutung der intuition-istischen Logik // Math. Zeitschrift. Vol. 35. 1932; Tarski A. Der Aussagenkalkul und die Topologie // Fundamenta Mathematicae. Vol. 31. 193; Curry H.B. Combinatory Logic. Vol. 2. New York, 1968.

Энциклопедия эпистемологии и философии науки. М.: «Канон+», РООИ «Реабилитация». . 2009.

Нужно сделать НИР?

Полезное


Смотреть что такое "интуиционистская логика" в других словарях:

  • ИНТУИЦИОНИСТСКАЯ ЛОГИКА — одна из наиболее важных ветвей неклассической логики, имеющая своей филос. предпосылкой программу интуиционизма. Выдвигая на первый план математическую интуицию, интуиционисты не придавали большого значения систематизации логических правил.… …   Философская энциклопедия

  • ИНТУИЦИОНИСТСКАЯ ЛОГИКА — логика, удовлетворяющая интуиционистским требованиям к математическим рассуждениям …   Большой Энциклопедический словарь

  • Интуиционистская логика — Интуиционизм  система философских и математических идей и методов, связанных с пониманием математики как совокупности «интуитивно убедительных» умственных построений. С точки зрения интуиционизма, основным критерием истинности математического… …   Википедия

  • интуиционистская логика — логика, удовлетворяющая интуиционистским требованиям к математическим рассуждениям. * * * ИНТУИЦИОНИСТСКАЯ ЛОГИКА ИНТУИЦИОНИСТСКАЯ ЛОГИКА, логика, удовлетворяющая интуиционистским требованиям к математическим рассуждениям …   Энциклопедический словарь

  • Интуиционистская логика —         форма логики предикатов (См. Логика предикатов), отражающая взгляд Интуиционизма на характер логических законов, считающихся, с его точки зрения, допустимыми в применении к доказательствам суждений из тех частей дедуктивных наук (особенно …   Большая советская энциклопедия

  • интуиционистская логика — одна из наиболее важных ветвей логики неклассической, имеющая своей философской предпосылкой программу интуиционизма. Выдвигая на первый план математическую интуицию, интуиционисты не придавали большого значения систематизации логических правил.… …   Словарь терминов логики

  • ИНТУИЦИОНИСТСКАЯ ЛОГИКА — совокупность приемлемых с точки зрения интуиционизма методов доказательства утверждений. В более узком смысле под И. л. понимается интуиционистское исчисление предикатов, сформулированное А. Рейтингом (A. Heyting) в 1930. Это исчисление… …   Математическая энциклопедия

  • ЛОГИКА В РОССИИ — эволюция современной (математической) логики в России. Кон. 19 в. и нач. 20 в. знаменуют выход логики за рамки силлогистики и появление логиков новаторов, таких как П.С. Порецкий, М.В. Каринский, Л.В. Рутковский, СИ. Поварнин, и др. Казанский… …   Философская энциклопедия

  • ЛОГИКА — (от греч. logos слово, понятие, рассуждение, разум), или Формальная логика, наука о законах и операциях правильного мышления. Согласно основному принципу Л., правильность рассуждения (вывода) определяется только его логической формой, или… …   Философская энциклопедия

  • ЛОГИКА СИМВОЛИЧЕСКАЯ —     ЛОГИКА СИМВОЛИЧЕСКАЯ математическая логика. теоретическая логика область логики, в которой логические выводы исследуются посредством логических исчислений на основе строгого символического языка. Термин “символическая логика” был, по видимому …   Философская энциклопедия


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»